M1 || M2
== M1 ||decl M2
== & 1of(2of(2of(M1))) || 1of(2of(2of(M2)))
== & 1of(2of(2of(2of(M1)))) || 1of(2of(2of(2of(M2))))
== & 1of(2of(2of(2of(2of(M1))))) || 1of(2of(2of(2of(2of(M2)))))
== & 1of(2of(2of(2of(2of(2of(M1)))))) || 1of(2of(2of(2of(2of(2of(M2))))))
== & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(2of(2of(2of(2of(2of(2of(M2)))))))
== & 1of(2of(2of(2of(2of(2of(2of(2of(M1)))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))
== & 1of(2of(2of(2of(2of(2of(2of(2of(2of(M1))))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(2of(
== & 1of(2of(2of(2of(2of(2of(2of(2of(2of(M1))))))))) || 1of(M2)))))))))
== & 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== & 1of(M1)))))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2))))))))))
== & 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== & 1of(M1))))))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2))))))))))) 

latex

---

clarification:

ma-compatible{i:l}
ma-compatible(M1; M2)
== ma-compatible-decls{i:l}
== ma-compatible-decls(M1; M2)
== & fpf-compatible(Id;
== & fpf-compatible(x.fpf-cap(fpf-join(IdDeq;1of(M1);1of(M2));IdDeq;x;Void);
== & fpf-compatible(IdDeq;
== & fpf-compatible(1of(2of(2of(M1)));
== & fpf-compatible(1of(2of(2of(M2))))
== & fpf-compatible(Id;
== & fpf-compatible(a.(State(fpf-join(IdDeq;1of(M1);1of(M2)))
== & fpf-compatible(fpf-cap(fpf-join(KindDeq;1of(2of(M1));1of(2of(M2)));KindDeq;locl(a);Top)
== & fpf-compatible(Prop{i});
== & fpf-compatible(IdDeq;
== & fpf-compatible(1of(2of(2of(2of(M1))));
== & fpf-compatible(1of(2of(2of(2of(M2)))))
== & fpf-compatible((KndId);
== & fpf-compatible(kx.(State(fpf-join(IdDeq;1of(M1);1of(M2)))
== & fpf-compatible(Valtype(fpf-join(KindDeq;1of(2of(M1));1of(2of(M2)));1of(kx))
== & fpf-compatible(fpf-cap(fpf-join(IdDeq;1of(M1);1of(M2));IdDeq;2of(kx);Void));
== & fpf-compatible(product-deq(Knd;Id;KindDeq;IdDeq);
== & fpf-compatible(1of(2of(2of(2of(2of(M1)))));
== & fpf-compatible(1of(2of(2of(2of(2of(M2))))))
== & fpf-compatible
== ((KndIdLnk);
== (kl.((tg:Id
== (kl.(((State(fpf-join(IdDeq;1of(M1);1of(M2)))
== (kl.(((Valtype(fpf-join(KindDeq;1of(2of(M1));1of(2of(M2)));1of(kl))
== (kl.((((fpf-cap(fpf-join(KindDeq;1of(2of(M1));1of(2of(
== (kl.((((fpf-cap(fpf-join(KindDeq;1of(2of(M1));1of(M2)));KindDeq;rcv(2of(
== (kl.((((fpf-cap(fpf-join(KindDeq;1of(2of(M1));1of(M2)));KindDeq;rcv(kl),tg);Void) List))) List);
== (product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== (1of(2of(2of(2of(2of(2of(M1))))));
== (1of(2of(2of(2of(2of(2of(M2)))))))
== & fpf-compatible(Id;
== & fpf-compatible(x.(Knd List);
== & fpf-compatible(IdDeq;
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(M1)))))));
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(M2))))))))
== & fpf-compatible((IdLnkId);
== & fpf-compatible(lt.(Knd List);
== & fpf-compatible(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(2of(M1))))))));
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))
== & fpf-compatible(Knd;
== & fpf-compatible(k.(Id List);
== & fpf-compatible(KindDeq;
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(2of(2of(M1)))))))));
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(2of(2of(M2))))))))))
== & fpf-compatible(Knd;
== & fpf-compatible(k.(IdLnk List);
== & fpf-compatible(KindDeq;
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M1))))))))));
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))))
== & fpf-compatible(Id;
== & fpf-compatible(x.(Knd List);
== & fpf-compatible(IdDeq;
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M1)))))))))));
== & fpf-compatible(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))))) 

latex

Definitions	M1 ||decl M2, locl(a), Top, Prop, State(ds), x:AB(x), Valtype(da;k), f(x)?z, f  g, rcv(l,tg), Void, x:AB(x), product-deq(A;B;a;b), IdLnkDeq, P & Q, IdLnk, KindDeq, f || g, Id, type List, Knd, IdDeq, 1of(t), 2of(t)
FDL editor aliases	ma-compatible